COMMENT ⊗   VALID 00016 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	some notions of set theory
C00005 00003	propositional schemata, used by the rewriter to normalize expressions
C00007 00004	use Landau, Grundlagen, Chapter I, theorems 1-9
C00012 00005	(proof ordering)
C00023 00006	(multiplication)theorems 28-36
C00027 00007	(proof all)
C00034 00008	(proof commutaddition)
C00035 00009	proof of other facts about addition
C00036 00010	(proof trichotomy)
C00039 00011	quick proof
C00043 00012	trichotomy is an exclusive disjunction:
C00046 00013	trichotomy: conclusion
C00047 00014	transitivity of order
C00049 00015	Landau_bis_th15
C00051 00016	bound quantifiers
C00060 ENDMK
C⊗;
;some notions of set theory
(wipe-out)
(proof sets)

(decl (arb arb1 arb2) (type: |?arbitrary|))
(decl (setvar setvar1) (type: |?arbitrary→truthval|))
(decl epsilon (type: |@arb⊗@setvar→truthval|) (infixname: ε) (bindingpower: 925))
(define epsilon |∀arb1 obj1.arb1εobj1≡obj1(arb1)|)
(label epsilondef)

;(decl epsilon (type: |ground⊗@set→truthval|) (infixname: ε) (bindingpower: 925))
;(define epsilon |∀a xv.xvεa≡a(xv)|)
;(label epsilondef)

(axiom |∀setvar setvar1.(∀arb.arbεsetvar≡arbεsetvar1)⊃setvar=setvar1|)
(label set_extensionality)

(decl function (type: |?arbitrary*→?arbitrary|)(syntype: variable))
(decl zeta (type: |?arbitrary*→truthval|)(syntype: variable))
(decl parvar (type:|?arbitrary|)(syntype: variable))
(axiom |(∀arb1.∃arb2.zeta(arb1,arb2,parvar))⊃
        (∃function.∀arb1.zeta(arb1,function(arb1,parvar),parvar))|)
(label choice)

;propositional schemata, used by the rewriter to normalize expressions
(proof normal)

(axiom  |∀p p1 p2.((p∨p1)∧p2)≡((p∧p2)∨(p1∧p2))|)
(label normal)
(axiom  |∀p p1 p2.(p2∧(p∨p1))≡((p2∧p)∨(p2∧p1))|)
(label normal)
(axiom  |∀p p1 p2.(p2∧(p∨p1))≡((p∧p2)∨(p1∧p2))|)
(label normal)
(axiom |∀p p1 p2.(p∨p1⊃p2)≡(p⊃p2)∧(p1⊃p2)|)
(label normal)

(axiom  |∀p p1.(¬(p∨p1))≡((¬p)∧(¬p1))|)
(label demorgan)

(axiom |∀P p1.¬(P∧p1)≡¬P∨¬p1|)
(label demorgan1)

;It would cause combinatorial explosion,to add these to simpinfo, or to put everything,
;say,in conjunctive normal form. So we call them as rewriters when needed.

;a few tricks

(axiom |∀p p1.p≡(p1⊃p)∧(¬p1⊃p)|)
(label excluded_middle)

;(derive |∀p p1 p2.(p1⊃p2)∧(if p then p1 else p2)⊃p2|)
(axiom |∀p p1 p2.(p1⊃p2)∧(if p then p1 else p2)⊃p2|)
(label trans_cond)

;(trw |∀p1 p2 p3 p4.(p2≡p4)∧(p1∨p2∨p3)⊃p1∨p4∨p3|)
(axiom |∀p1 p2 p3 p4.(p2≡p4)∧(p1∨p2∨p3)⊃p1∨p4∨p3|)
(label disjunct_subst)
;∀P1 P2 P3 P4.(P2≡P4)∧(P1∨P2∨P3)⊃P1∨P4∨P3

;(trw |∀p p1 p2.p∧p1⊃¬p2≡¬(p∧p1∧p2)|)
(axiom |∀p p1 p2.p∧p1⊃¬p2≡¬(p∧p1∧p2)|)
(label inconsistent)
;use Landau, Grundlagen, Chapter I, theorems 1-9
(proof natnum)

(decl (i j k n m) (sort: natnum) (type: ground))
(decl (a b c set) (type: |ground→truthval|))
(decl add1 (type: |ground→ground|) (syntype: constant) (postfixname: |'|)
      (bindingpower: 975))

;Landau_ax1
(trw |natnum 0|)

;Landau_ax2
(axiom |∀n.natnum(n')|)
(label simpinfo)

;Landau_ax3
(axiom  |∀n.¬(n'=0)|)
(label zero_not_successor) (label succfacts)

;Landau_ax4
(axiom |∀n m.(n'=m')≡(n=m)|)
(label successoreq) (label succfacts)

;Landau ax5
(axiom |∀a.a(0)∧(∀n.a(n)⊃a(n'))⊃(∀n.a(n))|)
(label proof_by_induction)

(label simpinfo succfacts)

(derive |∀m n.m≠n⊃m'≠n'| successoreq)
(label Landau_th1)

(ue (a |λn.n≠n'|) proof_by_induction (use successoreq))
(label Landau_th2)

(ue (a |λn.n≠0⊃∃k.n=k'|) proof_by_induction)
(label Landau_th3)

;Landau_def1
(decl plus (infixname: |+|) (type: |ground⊗ground⊗ground*→ground|) (syntype: constant)
      (associativity: both) (bindingpower: 930))    
(defax plus |∀n k.0+n=n∧k'+n=(k+n)'|)
(label simpinfo) (label plusfacts)

;(ue (a |λn.∀m.natnum(n+m)|) proof_by_induction)
(axiom |∀n m.natnum(n+m)|) proof_by_induction)
(label simpinfo)
        
;(trw |∀n m.∃k.k=n+m ∧ (∀i j.i=m+n ∧ j=m+n ⊃ i=j)|)
(axiom |∀n m.∃k.k=n+m ∧ (∀i j.i=m+n ∧ j=m+n ⊃ i=j)|)
(label Landau_th4)

;Landau_th5
;associativity has been declared
;(trw |∀n m k.(n + m) + k = n + (m + k)|)

;Landau's th6 is in proof commutaddition; see below
(axiom |∀n.n+0=n|)
(label simpinfo) (label plusfacts)

;the effect of the following axiom is to force sums in basically normal
;form: the "simpler" terms will come first

(axiom |∀k n.k+n=n+k|)
(label commutadd) (label plusfacts)

;(ue (a |λn.n≠n+m'|) proof_by_induction successoreq)
(axiom |∀n m.n≠n+m'|)
(label Landau_th7)

;(ue (a |λn.∀k m.k≠m⊃n+k≠n+m|) proof_by_induction)
(axiom |∀n k m.k≠m⊃n+k≠n+m|)
(label Landau_th8)
                
(axiom |∀n m.m=n∨(∃k.m=n+k')∨(∃k.n=m+k')|) 
(label tricotomy)(label trct0)

(axiom |∀n m.m=n⊃¬(∃k.m=n+k')∧¬(∃k.n=m+k')|)
(label tricotomy)(label trct1)

(axiom |∀n m.(∃k.m=n+k')⊃¬m=n∧¬(∃k.n=m+k')|)
(label tricotomy)(label trct2)

(axiom |∀n m.(∃k.n=m+k')⊃¬m=n∧¬(∃k.m=n+k')|)
(label tricotomy)(label trct3)

(label simpinfo plusfacts)
;proofs of the following facts below

(axiom |∀n.1+n=n'∧n+1=n'|)
(label simpinfo) (label plusfacts) (label plusdef1)

(axiom |∀n k.n+k'=(n+k)'|)
(label simpinfo) (label plusfacts)
;exercise

(axiom |∀n k m.(k+m=k+n)≡(m=n)|)
(label lpluscan) (label plusfacts)

(axiom |∀n k m.(m+k=n+k)≡(m=n)|)
(label rpluscan) (label plusfacts)

(axiom |∀n k.n+k=0≡n=0∧k=0|)
(label addtozero) (label plusfacts)
(show *)
(proof ordering)

(decl lessp (type: |ground⊗ground→truthval|) (syntype: constant) (infixname: <)
      (bindingpower: 920))
(decl greaterp (type: |ground⊗ground→truthval|) (syntype: constant) (infixname: >)
      (bindingpower: 920))
(defax greaterp |∀n m.n>m≡∃k.n=m+k'|)
(label Landau_def2)

;Landau_def3
(defax lessp |∀n m.n<m≡∃k.m=n+k'|)


(axiom |∀n m.m<n∨m=n∨m>n|)
(label totalord)
;(label simpinfo)

;Landau_a_th10
(axiom |∀n m.m=n⊃¬(m<n)∧¬(m>n)|)
(label strict1)
;(label simpinfo)
         
;Landau_b_th10
(axiom |∀n m.(m>n)⊃¬m=n∧¬(m<n)|)
(label strict2)
;(label simpinfo)
           
;Landau_c_th10
(axiom |∀n m.(m<n)⊃¬m=n∧¬(m>n)|)
(label strict3)
;(label simpinfo)
(label simpinfo plusfacts)

;Landau_th11 and 12
;(trw |∀n m.(m>n)≡(n<m)| (open lessp greaterp))
(axiom |∀n m.(m>n)≡(n<m)|)
(label greaterp_lessp)
(label simpinfo)

(decl grteqp (type: |ground⊗ground→truthval|) (syntype: constant) (infixname: ≥)
      (bindingpower: 920))

(decl lsseqp (type: |ground⊗ground→truthval|) (syntype: constant) (infixname: ≤)
      (bindingpower: 920))

;Landau_def4
(defax grteqp |∀n m.(m≥n)≡(m>n)∨(m=n)|)

;Landau_def5
(defax lsseqp |∀n m.(m≤n)≡(m<n)∨(m=n)|)

;Landau_th13 and 14
;(derive |∀n m.m≥n≡n≤m| greaterp_lessp (open grteqp lsseqp))
(axiom |∀n m.m≥n≡n≤m|)
(label grteqp_lsseqp)
(label simpinfo)

;Landau_th15
(axiom |∀n m k.n<m ∧ m<k ⊃ n<k|)
(label transitivity_of_order)
;see proof below

;Landau_bis_th15
(axiom |∀n m k.(k>m)∧(m>n)⊃(k>n)|)
(label transitivity_of_greaterp)
                       
;Landau_a_th16
;(derive |∀n m k.n≤m ∧ m<k ⊃ n<k|  transitivity_of_order 
;        (open lsseqp) (use normal mode: exact))
(axiom |∀n m k.n≤m ∧ m<k ⊃ n<k|)
(label lsseqp_lessp_lessp)

;Landau_b_th16
;(derive |∀n m k.n<m ∧ m≤k ⊃ n<k|  transitivity_of_order 
;        (open lsseqp) (use normal mode: exact))
(axiom |∀n m k.n<m ∧ m≤k ⊃ n<k|)
(label lessp_lsseqp_lessp)

;Landau_th17
(axiom |∀n m k.(n≤m)∧(m≤k)⊃(n≤k)|)
(label transitivity_of_lsseqp)

;Landau_th18
;(trw |∀n m.n+m'>n| (open greaterp))
(axiom |∀n m.n+m'>n|)
(label increasing)

(axiom |∀n m.n'<m'≡n<m|)
(label successorless) (label succfacts)(label simpinfo)

;Landau_th19 and th20
(axiom |∀n m k.m+k>n+k≡m>n|)
(label rplus_greatcan)(label plusfacts)

(axiom |∀n m k.m+k<n+k≡m<n|)
(label rplus_lesscan)(label plusfacts)
                                
;the analogue statement with equal is rpluscan

;(trw |∀n m k.n>m⊃k+n>k+m| Landau_a_th19 (part 1(part 2(use commutadd mode: exact))))
;(label bis_th19)

(axiom |∀N M I J.N>M∧I>J⊃N+I>M+J|)
(label Landau_th21)

(axiom |∀n m i j.n≥m∧i>j⊃n+i>m+j|)
(label Landau_a_th22)

(axiom |∀n m i j.n>m∧i≥j⊃n+i>m+j|)
(label Landau_b_th22)

(axiom |∀n m i j.(n≥m)∧(i≥j)⊃(n+i≥m+j)|)
(label Landau_th23)

(axiom |∀n.n≥0|)
(label Landau_a_th24)

;(rw landau_a_th24 (open grteqp))
;∀N.N>0∨N=0

;(derive |∀n.¬n<0| (strict3 *))
(axiom |∀n.¬n<0|)
(label zeroleast1)(label succfacts)

;(derive |∀n.n≠0⊃0<n| (totalord zeroleast1) 
;        (use greaterp_lessp mode: exact direction: reverse))
(axiom |∀n.¬n=0⊃0<n|)
(label zeroleast2) (label succfacts)
 
(axiom |∀n.n'≥1| )
(label Landau_b_th24)

(axiom |∀n m.n>m⊃n≥m'|)
(label Landau_th25)

(axiom |∀m n.m<n'⊃m≤n|)
(label Landau_th26)

;(decl epsilon (type: |ground⊗@set→truthval|) (infixname: ε) (bindingpower: 925))
;(define epsilon |∀a n.nεa≡a(n)|)
;(label epsilondef)

(axiom |∀a.(∃m.a(m))⊃(∃n.a(n)∧(∀m.a(m)⊃n<m))|)
(label Landau_th27)
(show *)
;(multiplication);theorems 28-36
(proof multip)

(decl times (type: |ground⊗ground⊗ground*→ground|) (syntype: constant)
      (infixname: |*|) (associativity: both)(bindingpower: 935))
(defax times |∀n k.0*n=0∧n'*k=(n*k)+k|)
(label simpinfo) (label timesfacts)(label Landau_def6)

;(trw |∀n m1 m2.m1=m2⊃n*m1=n*m2|) 
;(label Landau_b_th32)

;(ue (a |λn.∀m.natnum(n*m)|) proof_by_induction (open times))
(axiom |∀n m.natnum(n*m)|)
(label simpinfo)

;(ue (a |λn.n*0=0∧0'*n=n∧n*0'=n|) proof_by_induction (open times))
(axiom |∀n.n*0=0∧1*n=n∧n*1=n|) 
(label simpinfo) (label timesfacts)

(axiom |∀k n.n*k'=n*k+n|) 
(label timsucc) (label timesfacts)

;times cancellation (part b of Landau theorem 33)

(axiom |∀n k m.¬k=0⊃((k*m=k*n)≡(m=n))|)
(label ltimescan) (label timesfacts)

(axiom |∀n k m.¬k=0⊃((m*k=n*k)≡(m=n))|)
(label rtimescan) (label timesfacts)

;commutativity (Landau theorem 29)
 
(axiom |∀n m.n*m=m*n|)
(label commutmult) (label timesfacts)

;(trw |∀n m.∃k.k=n*m|)
;(label Landau_th28)

(axiom |∀n k.¬n=0⊃n*k=0≡k=0|)
(label ltimestozero) (label timesfacts)

(axiom |∀n k.¬n=0⊃k*n=0≡k=0|)
(label rtimestozero) (label timesfacts)

(derive |n≠0∧m≠0⊃n*m≠0| rtimestozero)
(label nozerodivisors)(label timesfact)

;distributivity (Landau th30)

(axiom |∀n k m.n*(k+m)=n*k+n*m|) 
(label ldistrib) (label timesfacts) (label plusfacts)

(axiom |∀n m k.(m+k)*n=m*n+k*n|)
(label rdistrib) (label timesfacts) (label plusfacts)

;(derive |∀n m1 m2.m1=m2⊃m1*n=m2*n|)
;(label Landau_c_th32)

(axiom |∀N M K.N>M∧¬K=0⊃N*K>M*K|)
(label Landau_a_th32)

(axiom |∀n m k.N<M∧k≠0⊃N*K<M*K|)
(label Landau_d_th32)
	
(axiom |∀n m k.K≠0∧M*K>N*K⊃M>N|)
(label Landau_a_th33)

(axiom |∀n m k.¬K=0∧M*K=N*K⊃M=N|)
(label Landau_b_th33)

(axiom |∀n m k.K≠0∧M*K<N*K⊃M<N|)
(label Landau_c_th33)

(axiom |∀N M I J.N>M∧I>J⊃N*I>M*J|)
(label landau_th34)

(axiom	|∀n m i j.M≠0∧N≥M∧I>J⊃N*I>M*J|)
(label Landau_a_th35)

(axiom |∀n m i j.J≠0∧N>M∧I≥J⊃N*I>M*J|)
(label Landau_b_th35)

(axiom |∀N M I J.N≥M∧I≥J⊃N*I≥M*J|)
(label Landau_th36)
(show *)
(proof all)

(decl all (type: |ground⊗@set→truthval|) (syntype: constant))
(decl some (type: |ground⊗@set→truthval|) (syntype: constant))
;axiom for all
(defax all |∀n a.all(0,a)∧(all(n',a)≡a(n)∧all(n,a))|)
(label alldef)

;axiom for some
(defax some |∀n a.¬some(0,a)∧(some(n',a)≡a(n)∨some(n,a))|)
(label somedef)

;properties of all and some

(axiom |∀a n.(∀m.m<n⊃a(m))≡all(n,a)|)
(label allfact)

(axiom |∀a n.(∃m.m<n∧a(m))≡some(n,a)|)
(label somefact)

(save-proofs nat)
(proof commutaddition)
(unlabel simpinfo plusfacts) ;delete plusfacts from simpinfo temporarily

(ue (a |λn.∀k.n+k'=(n+k)'|) proof_by_induction (open plus))
;∀N K.N+K'=(N+K)'
(label plushelp)

(ue (a |λn.n+0=n|) proof_by_induction (open plus))
;∀N.N+0=N
(label pluszero)

(ue (a |λk.∀n.n+k=k+n|) proof_by_induction  (open plus) (use plushelp pluszero))
;∀N N3.N3+N=N+N3
(label commutadd)

;proof of other facts about addition
(ue (a |λn.1+n=n'∧n+1=n'|) proof_by_induction 
    (open plus)(part 1(use commutadd mode: exact)))
;∀N.1+N=N'∧N+1=N'

(ue (a |λn.n+k'=(n+k)'|) proof_by_induction (open plus))
;∀N.N+K'=(N+K)'

(ue (a |λn.(n+m=n+k)≡(m=k)|) proof_by_induction (open plus))
;∀N.N+M=N+K≡M=K

(rw * (use commutadd mode: exact))
;∀N.M+N=K+N≡M=K

(ue (a |λn.n+k=0≡n=0∧k=0|) proof_by_induction 
    (open plus) zero_not_successor)
;∀N.N+K=0≡N=0∧K=0

(proof trichotomy)

;we use the following result:
;labels: LANDAU_TH3 
;∀N.¬N=0⊃(∃K.N=K')

;the basis case follows by logic
(derive |0=m∨(∃k.m=0+k')∨(∃k.0=m+k')| landau_th3)
(label trc0)

;induction hypothesis:
(assume |n=m∨(∃k.m=n+k')∨(∃k.n=m+k')|) 
(label trc1)

;first case
(assume |n=m|)
(label trc2)

;the third disjunct is true:
(trw |n'=m∨(∃k.m=n'+k')∨(∃k.n'=m+k')| * )
;(∃K.M=N'+K')∨(∃K.N'=M+K')
(label trc3)

;second case
(assume |(∃k.m=n+k')|)
(define kv |m=n+kv'| *)
;KV is unknown.
;the symbol KV is given the same declaration as K
(label trc4)

;a subargument by cases:
(assume |kv=0|)
(rw trc4 *)
;M=N'
(trw |n'=m∨(∃k.m=n'+k')∨(∃k.n'=m+k')| * )
;N'=M∨(∃K.M=N'+K')∨(∃K.N'=M+K')
(label trc5)

(assume |kv≠0|)
(define jv |kv=jv'| (* landau_th3))
;JV is unknown.
;the symbol JV is given the same declaration as J
;using again our theorem we obtain an element jv...

(rw trc4 (use * mode: exact))
;M=((N+JV)')'

(trw |m=n'+jv'| *)
;M=N'+JV'

;...that makes the second disjunct true:
(trw |n'=m∨(∃k.m=n'+k')∨(∃k.n'=m+k')| * )
;N'=M∨(∃K.M=N'+K')∨(∃K.N'=M+K')
(label trc6)

;conclude the subargument:
(trw |kv=0∨kv≠0|)
;KV=0∨¬KV=0
(cases * trc5 trc6)
;N'=M∨(∃K.M=N'+K')∨(∃K.N'=M+K')
(label trc7)
 
;third case:
(assume |(∃k.n=m+k')|)
(define mv |n=m+mv| *)
;MV is unknown.
;the symbol MV is given the same declaration as M

(trw |n'=m+mv'| *)
;N'=M+MV'

(trw |n'=m∨(∃k.m=n'+k')∨(∃k.n'=m+k')| * )
;N'=M∨(∃K.M=N'+K')∨(∃K.N'=M+K')
(label trc8)
 
;conclude the induction step:
(cases trc1 trc3 trc7 trc8)
;N'=M∨(∃K.M=N'+K')∨(∃K.N'=M+K')
;deps: (TRC1)

(ci trc1)
;N=M∨(∃K.M=(K+N)')∨(∃K.N=(K+M)')⊃N'=M∨(∃K.M=((K+N)')')∨(∃K.N=K+M)

(ue (a |λn.n=m∨(∃k.m=n+k')∨(∃k.n=m+k')|) 
    proof_by_induction (trc0 *))
;∀N.N=M∨(∃K.M=(K+N)')∨(∃K.N=(K+M)')

;quick proof

(get-proofs nat)
;the following is a form of double induction

(axiom |∀a2.(∀n m.a2(0,n)∧a2(n,0)∧(a2(n,m)⊃a2(n',m')))⊃∀n m.a2(n,m)|)
(label proof_by_doubleinduction)

(setq rewritemessages t)
(ekl)
(ue (a |λn.n=0∨some(n,λk.n=k')|) proof_by_induction 
    (open some) (use normal mode: always))
;∀N.N=0∨SOME(N,λK.N=K')

(ue (a2 |λm n.n=m∨some(m,λk.m=n+k')∨some(n,λk.n=m+k')|) 
    proof_by_doubleinduction (open some) (use normal mode: always) *)
;∀N M.M=N∨SOME(N,λK.N=(K+M)')∨SOME(M,λK.M=(K+N)')

(rw * (use somefact mode: always direction: reverse))
;∀N M.M=N∨(∃M1.M1<N∧N=(M1+M)')∨(∃M2.M2<M∧M=(M2+N)')
;trichotomy is an exclusive disjunction:

;labels: LANDAU_TH7 
;∀N.¬N=N+M'

;trct1
(trw |n=m ⊃ ¬(∃k.m=n+k')∧ ¬(∃k.n=m+k')|  Landau_th7 
     (nuse commutadd plusfacts))
;N=M⊃¬(∃K.M=N+K')∧¬(∃K.N=M+K')

;a useful lemma
(assume |∃k.m=n+k'|)
(label excl1)
(define kv1 |m=n+kv1'| *)
;KV1 is unknown.
;the symbol KV1 is given the same declaration as KV
(label excl2)

(assume |∃k.n=m+k'|)
(label excl3)
(define kv2 |n=m+kv2| *)
;KV2 is unknown.
;the symbol KV2 is given the same declaration as KV

(rw * (use excl2 mode: exact))
;N=(N+KV1+KV2)'
;deps: (EXCL1 EXCL3)

(ue ((n.n)(m.|kv1+kv2|)) landau_th7 *)
;FALSE
(label excl)

(ci (excl1 excl3))
;¬((∃K.M=(K+N)')∧(∃K.N=(K+M)'))

(derive |(∃k.m=n+k')≡¬(∃k.n=m+k')| *)
(label excl)

;trct2
(derive |∀n m.(∃k.m=n+k')⊃¬m=n∧¬(∃k.n=m+k')| (trct1 excl))

;trct3
(derive |∀n m.(∃k.n=m+k')⊃¬m=n∧¬(∃k.m=n+k')| (trct1 excl))

;trichotomy: conclusion
(unlabel simpinfo plusfacts)
;totalord
(derive |∀n m.m=n∨(m<n)∨(m>n)| trct0 (open lessp greaterp))

;Landau_a_th10
;strict1
(derive |∀n m.m=n⊃¬(m<n)∧¬(m>n)| trct1 (open lessp greaterp))

;Landau_b_th10
;strict2
(derive |∀n m.(m>n)⊃¬m=n∧¬(m<n)| trct2 (open lessp greaterp))

;Landau_c_th10
;strict3
(derive |∀n m.(m<n)⊃¬m=n∧¬(m>n)| trct3 (open lessp greaterp))

;transitivity of order
(proof transitivity)

(unlabel simpinfo plusfacts)
(assume |n < m ∧ m < k|)
(label tr1)

(rw * (open lessp))
;(∃K.M=N+K')∧(∃K1.K=M+K1')
;deps: (TR1)
(label tr2)

(define kv1 |m=n+kv1'| *)
;KV1 is unknown.
;the symbol KV1 is given the same declaration as K
(label tr3)

(define kv2 |k=m+kv2| -2)
;KV2 is unknown.
;the symbol KV2 is given the same declaration as K
(label tr4)

(label simpinfo plusfacts)
(unlabel simpinfo commutadd)

(rw * (use -2 mode: exact))
;K=(N+KV1+KV2)'
;deps: (TR1)

(trw |n<k| (open lessp) * (use plusfacts mode: exact))
;N<K
;deps: (TR1)

(ci tr1)
;N<M∧M<K⊃N<K
(label simpinfo commutadd)
;Landau_bis_th15
;transitivity_of_greaterp
(trw |∀n m k.(k>m)∧(m>n)⊃(k>n)|  transitivity_of_order
     (use greaterp_lessp mode: exact))
;∀N M K.K>M∧M>N⊃K>N

;Landau_th17
;transitivity_of_lsseqp
(trw |∀n m k.(n≤m)∧(m≤k)⊃(n≤k)| (open lsseqp) (use normal mode: always)
     (transitivity_of_order))
;∀N M K.N≤M∧M≤K⊃N≤K

;the proofs of Theorems 19 and 20 are easily given by induction
;we could also expand the definitions 
    
(trw |∀n m.n'<m'≡n<m| (open lessp))
;∀N M.N'<M'≡N<M

(ue (a |λk.n+k<m+k≡n<m|) proof_by_induction (use successorless mode: exact))
;∀N2.N2+N<N2+M≡N<M

(trw |∀n m k.m+k>n+k≡m>n| * (use greaterp_lessp mode: exact))
;∀N M K.M+K>N+K≡M>N
;bound quantifiers
(proof allprop)

;we can easily prove that `all' does its job

(ue ((a.|λn.all(n,a)⊃(m<n⊃a(m))|)) proof_by_induction
     ((use transitivity_of_order) (use successor1) (open all)
       (use less_succ_lesseq normal mode: exact) (open lesseq)))
;∀N.ALL(N,A)⊃(M<N⊃A(M))

(ue ((a.|λn.(∀m.m<n⊃a(m))⊃all(n,a)|)) proof_by_induction (open all)
      (use normal mode: always)
      (use less_succ_lesseq mode: exact) (open lesseq)))
;∀N.(∀M.M<N⊃A(M))⊃ALL(N,A)

(derive |∀n.(∀m.m<n⊃a(m))≡all(n,a)| (* -2))

;similarly for `some':

(ue ((a.|λn.some(n,a)⊃(∃m.m<n∧a(m))|)) proof_by_induction
     ((use transitivity_of_order) (use successor1) (open some) (part 1 (der))
       (use less_succ_lesseq normal mode: exact) (open lesseq)))
;∀N.SOME(N,A)⊃(∃M.M<N∧A(M))

(ue ((a.|λn.(∃m.m<n∧a(m))⊃some(n,a)|)) proof_by_induction (open some)
      (use normal mode: always) (part 1(der))
      (use less_succ_lesseq mode: exact) (open lesseq)))
;∀N.(∃M.M<N∧A(M))⊃SOME(N,A)

(derive |∀n.(∃m.m<n∧a(m))≡some(n,a)| (* -2))